//MAX-SAT problem-depended class
//$Id: maxsat_bnb.h 671 2011-02-27 12:34:03Z Oleg.Bulychov $
#pragma once

#include "src/heo/include/console_color.h"
#include "src/heo/include/dynamic_bit_array.h"
#include "src/heo/include/array.h"
#include "projects/maxsat/maxsat.h"
#include "solvers/bnb/bnb_common.h"

//__________________________________________________________________________________
template<>
struct solution<MaxSat_Solution, bnb_tag>:
    public MaxSat_Solution
{
    typedef solution<MaxSat_Solution, bnb_tag> TSolution;

    template<class E>
    TCostType get_Ub(E* env) const
    {
        return env->problem_.clause_count_ - get_Cost();
    }
};
//__________________________________________________________________________________
struct MaxSat_BnB_Params
{
    float lb_weight_;
    float deep_weight_;
    float greedy_weight_;
    int   size_to_solve_now_;
    int   debug_out_rate_;

    MaxSat_BnB_Params():
        lb_weight_(),
        deep_weight_(),
        greedy_weight_(),
        size_to_solve_now_(),
        debug_out_rate_()
    {}

    static char const* get_Name() { return "/"; }//TODO review
    static char const* get_Section() { return "/"; }

    template<class V>
    void accept(V& v)
    {
        v(VAR_(lb_weight),          7/16.f);
        v(VAR_(deep_weight),        8/16.f);
        v(VAR_(greedy_weight),      1/16.f);
        v(VAR_(size_to_solve_now),  6);
        v(VAR_(debug_out_rate),     1);
    }
};
//__________________________________________________________________________________
//__________________________________________________________________________________
struct MaxSat_Branch
{
    typedef solution<MaxSat_Solution, bnb_tag> TSolution;
    typedef TSolution::TCostType TCostType;

    size_t id_;
    TCostType sat_left_;
    TCostType sat_right_;
    TCostType unsat_left_;
    TCostType unsat_right_;
    TCostType lb_left_;
    TCostType lb_right_;
    TCostType lb_max_;
    TCostType sat_max_;
};
//__________________________________________________________________________________
class MaxSat_BnB_Predictor
{
    typedef solution<MaxSat_Solution, bnb_tag> TSolution;
    typedef TSolution::TCostType TCostType;
public:
    Array<size_t> var_list_;

    MaxSat_Branch branch_;

    MaxSat_BnB_Predictor():
        branch_()
    {}

    static char const* get_Name() { return "predictor"; }
    static char const* get_Section() { return get_Name(); }

    template<class V>
    void accept(V& v)
    {
        v(var_list_);
    }

    template<class E>
    void init(E* env, random_generator& rnd)
    {
        var_list_.resize(env->problem_.dimension_);
    }

    template<class E>
    void pre_Calculate(E* env, random_generator& rnd)
    {
        MOMS moms;
        moms.weight_.resize(env->problem_.dimension_);
        for (int i = 0; i < env->problem_.dimension_; ++i)
        {
            var_list_[i]    = i;
            moms.weight_[i] = 0.f;
        }
        moms.calculate(env->problem_);
        std::stable_sort(var_list_.begin(), var_list_.end(), MOMS::Compare(moms));
    }


    template<class BNB, class Task>
    bool find_Branch(BNB& bnb, Task& task)
    {
        for (size_t i = 0; i < var_list_.size(); ++i)
        {
            if (!task.free_var_list_[var_list_[i]])
                continue;
            branch_.id_ = var_list_[i];
            task.get_Bounds(bnb, branch_);
            return true;
        }
        ASSERT_(!"something wrong");
        return false;
    }

private:
    /**
    MOMS is a branching heuristic that selects a
    variable among those that appear More Often in clauses of Minimum Size
    */
    struct MOMS
    {
        Array<float> weight_;

        void calculate(MaxSat_Problem const& pbm)
        {
            int const* clause = &pbm.data_[0];
            for (MaxSat_Problem::size_type i = 0; i < pbm.clause_count_; ++i)
            {
                int clause_length = *clause++;
                float w = 1.f - (clause_length - pbm.min_clause_size_) / float(pbm.max_clause_size_);
                for (int j = 0; j < clause_length; ++j)
                {
                    int lit = clause[j];
                    size_t id;
                    if (lit < 0)
                    {//!x 
                        id = -lit - 1;
                    }
                    else
                    {//x
                        id = lit - 1;
                    }
                    weight_[id] += w;
                }
                clause += clause_length;
            }
        }

        struct Compare
        {
            MOMS const& moms_;
            Compare(MOMS const& moms):
                moms_(moms)
            {}
            bool operator()(size_t left, size_t right) const
            {
                return moms_.weight_[left] > moms_.weight_[right];
            }
        };

    };
};
//__________________________________________________________________________________
//__________________________________________________________________________________
//__________________________________________________________________________________
//__________________________________________________________________________________
//__________________________________________________________________________________
//__________________________________________________________________________________
class MaxSat_BnB_Task:
    public ref_object,
    public lite_object
{
    typedef MaxSat_BnB_Task TTask;
    typedef solution<MaxSat_Solution, bnb_tag> TSolution;
    typedef TSolution::TCostType TCostType;

    friend class MaxSat_BnB_Predictor;

public:
    struct LessPriority
    {
        bool operator()(TTask const* pLeft, TTask const* pRight) const
        {
            return pLeft->priority_ < pRight->priority_;
        }
    };

protected:
    dynamic_bit_array<>     free_var_list_;
    dynamic_bit_array<>     fixed_var_value_;

    size_t                  id_;
    TCostType               lb_;
    TCostType               sat_;
    int                     dim_;
    float                   priority_;
    int                     dbg_magic_;

    struct Proxy
    {
        dynamic_bit_array<>& data_;
        TCostType cost_;
        bool changed_;
        unsigned hash_;
        bool hash_changed_;

        Proxy(dynamic_bit_array<>& data, TCostType cost):
            data_(data),
            cost_(cost),
            changed_(false),
            hash_(),
            hash_changed_(true)
        {}
    };
public:
    explicit MaxSat_BnB_Task():
        id_(size_t(-1)),
        lb_(),
        sat_(),
        dim_(),
        dbg_magic_(0xC001BEAF)
    {}

    template<class V>
    void accept(V& v)
    {
        v(free_var_list_);
        v(fixed_var_value_);
        v(id_);
        v(lb_);
        v(sat_);
        v(dim_);
        v(priority_);
        v(dbg_magic_);
        VERIFY_(0xC001BEAF == dbg_magic_);
    }

    TCostType get_LB() const { return lb_; }

    template<class E>
    void init(E* env, random_generator& rnd)
    {
        dim_ = env->problem_.dimension_;
        free_var_list_.resize(env->problem_.dimension_, 0, false);
        free_var_list_.set();
        fixed_var_value_.resize(env->problem_.dimension_);
        priority_ = 1.f;
    }
    
    template<class BNB>
    void show_Progress(BNB& bnb, int step)
    {
        if (!bnb.params_.debug_out_rate_)
            return;
        if (step % bnb.params_.debug_out_rate_ != 0)
            return;
#pragma omp critical(debug_output)
        {
            int rank = bnb.get_Rank();
            if (rank > 0)
                sys_api::Set_Console_Color(rank % 15 + 1);
            if (id_ != size_t(-1))
            {
                std::cout
                    << std::setw(2)
                    << rank << ":" << std::setw(5) << step
                    << ": x[" << std::setw(4) << id_ + 1
                    << "]=" << fixed_var_value_[id_]
                    << ", dim=" << dim_
                    << ", sat=" << sat_
                    << ", lb=" << lb_
                    << "; ub=" << bnb.best_ub_
                    << ", pq size=" << bnb.pq_.size()
                    << lf;
                //for (int i = 0; i < bnb.env_->problem_.dimension_; ++i)
                //{
                //    std::cout << (!free_var_list_[i] ? (fixed_var_value_[i] ? "1" : "0") : ".");
                //}
                //std::cout << lf;
            }
            else
            {
                std::cout << std::setw(2) << rank << ":" << std::setw(5) << step << ": root"
                    << ", dim=" << dim_
                    << ", ub=" << bnb.best_ub_
                    << lf;
            }
            if (rank > 0)
                std::cout << no_color;
        }
    }

    template<class BNB, class Predictor>
    bool branch(BNB& bnb, 
                Predictor& pred,
                typename BNB::TPriorityQueue::value_type this_task,
                int step)
    {
        if (!pred.find_Branch(bnb, *this))
            return false;
        if (1 == dim_)
            return solve_Now(bnb, pred, step);

        //:make right: new variable = 1
        ref_ptr<MaxSat_BnB_Task> new_task;
        new_task.attach(new MaxSat_BnB_Task);
        new_task->init(bnb.env_, bnb.rnd_);
        if (!new_task->make_Right(bnb, pred, *this))
            return false;
        ++bnb.stat_.nodes_;

        if (new_task->lb_ < bnb.best_ub_)
        {
            bnb.pq_.push(new_task);
        }
        else
        {
            ++bnb.stat_.pruned_;
#ifdef BNB_LOG
#pragma omp critical(debug_output)
            {
                std::cout << std::setw(2) << bnb.get_Rank() << ":" << std::setw(5) << step
                    << ": RIGHT PRUNED: lb=" << new_task->lb_ << " >= " << bnb.best_ub_ << "=ub" << lf;
            }
#endif
        }

        //:make left from self: new variable = 0
        if (!make_Left(bnb, pred))
            return false;
        ++bnb.stat_.nodes_;
        if (lb_ < bnb.best_ub_)
        {
            bnb.pq_.push(this_task);
        }
        else
        {
            ++bnb.stat_.pruned_;
#ifdef BNB_LOG
#pragma omp critical(debug_output)
            {
                std::cout << std::setw(2) << bnb.get_Rank() << ":" << std::setw(5) << step
                    << ": LEFT PRUNED: lb=" << lb_ << " >= " << bnb.best_ub_ << "=ub" << lf;
            }
#endif
        }
        return true;
    }

private:
    void copy_To(TSolution& sol, TCostType cost)
    {
        Proxy p(fixed_var_value_, cost);
        sol.assign(p);
    }

    void set_Fixed_Var(size_t id)
    {
        ASSERT_(!free_var_list_[id]);
        ASSERT_(!fixed_var_value_[id]);
        fixed_var_value_.set(id);
    }

    bool get_Fixed_Var(size_t id)
    {
        ASSERT_(!free_var_list_[id]);
        return fixed_var_value_[id];
    }

    void fix_Var(size_t id)
    {
        ASSERT_(free_var_list_[id]);
        free_var_list_.set(id, 0);
    }

    template<class BNB, class Predictor>
    bool make_Right(BNB& bnb,
                    Predictor& pred,
                    MaxSat_BnB_Task& parent)
    {
        id_ = pred.branch_.id_;
        dim_ = parent.dim_ - 1;
        lb_ = pred.branch_.lb_right_;
        sat_ = pred.branch_.sat_right_;
        free_var_list_   = parent.free_var_list_;
        fixed_var_value_ = parent.fixed_var_value_;
        fix_Var(pred.branch_.id_);
        set_Fixed_Var(pred.branch_.id_);
        calc_Priority(bnb, pred);
        return true;
    }

    template<class BNB, class Predictor>
    bool make_Left(BNB& bnb,
                   Predictor& pred)
    {
        id_ = pred.branch_.id_;
        --dim_;
        lb_ = pred.branch_.lb_left_;
        sat_ = pred.branch_.sat_left_;
        fix_Var(pred.branch_.id_);
        //:value already set to 0;
        calc_Priority(bnb, pred);
        return true;
    }

    template<class BNB, class Predictor>
    void calc_Priority(BNB& bnb,
                       Predictor& pred)
    {
        if (dim_ <= bnb.params_.size_to_solve_now_)
        {
            priority_ = 100.f - float(dim_) / bnb.params_.size_to_solve_now_;
            return;
        }
        //TODO : update dynamically
        //:e.g. if low mem - increase deep_weight_?
        //TODO : non-linear?
        priority_ =
            bnb.params_.lb_weight_ * (1.f - (bnb.first_ub_ ? (float(lb_) / bnb.first_ub_) : 0.f)) + //:higher lb
            bnb.params_.deep_weight_ * (1.f - float(dim_) / bnb.env_->problem_.dimension_) +//:deep search
            bnb.params_.greedy_weight_ * (float(sat_) / bnb.env_->problem_.clause_count_);//:greedy

            //1.f - (bnb.first_ub_ ? (float(lb_) / bnb.first_ub_) : 0.f);//:higher lb
            //1.f - float(dim_) / bnb.env_->problem_.dimension_;//:deep search
            //float(sat_) / bnb.env_->problem_.clause_count_;//:greedy
    }

    template<class BNB, class Predictor>
    bool solve_Now(BNB& bnb,
                   Predictor& pred,
                   int step)
    {
        ASSERT_(dim_ == 1);
        TCostType cur_cost = bnb.current_.get_Cost();
        if (pred.branch_.sat_max_ > cur_cost)
        {
            TCostType ub = bnb.env_->problem_.clause_count_ - pred.branch_.sat_max_;
            if (ub < bnb.best_ub_)
                bnb.best_ub_ = ub;
            int rank = bnb.get_Rank();
            if (rank < bnb.get_Debug_Level())
            {
#pragma omp critical(debug_output)
                {
                    if (rank)
                        std::cout << color<red, ltgray>;
                    else
                        std::cout << color<ltred, white>;
                    std::cout << std::setw(2) << rank << ":" << std::setw(5) << step
                        << ">>>BETTER: cost="
                        << pred.branch_.sat_max_
                        << "; ub="
                        << bnb.best_ub_
                        << lf;
                    //for (int i = 0; i < bnb.env_->problem_.dimension_; ++i)
                    //{
                    //    std::cout << (!free_var_list_[i] ? (fixed_var_value_[i] ? "1" : "0") : ".");
                    //}
                    //std::cout << lf;
                    std::cout << no_color;
                }
            }

            if (pred.branch_.sat_right_ > pred.branch_.sat_left_ &&
                pred.branch_.sat_right_ > cur_cost)
            {
                fix_Var(pred.branch_.id_);
                set_Fixed_Var(pred.branch_.id_);
            }
            copy_To(bnb.current_, pred.branch_.sat_max_);
        }
        return true;
    }

    template<class BNB>
    void get_Bounds(BNB& bnb, MaxSat_Branch& b)
    {
        b.sat_left_ = b.unsat_left_ = b.sat_right_ = b.unsat_right_ = 0;

        int const* clause = &bnb.env_->problem_.data_[0];
        for (MaxSat_Problem::size_type i = 0; i < bnb.env_->problem_.clause_count_; ++i)
        {
            int clause_length = *clause++;
            enum EClauseType {CLAUSE_UNSAT, CLAUSE_SAT, CLAUSE_UNKNOWN};
            EClauseType clause_left  = CLAUSE_UNSAT;
            EClauseType clause_right = CLAUSE_UNSAT;

            for (int j = 0; j < clause_length; ++j)
            {
                int lit = clause[j];
                if (lit < 0)
                {//!x
                    size_t id = -lit - 1;
                    if (b.id_ == id)
                    {
                        ASSERT_(free_var_list_[id]);
                        clause_left = CLAUSE_SAT;//:left - x[id] = 0
                        if (clause_right != CLAUSE_UNSAT)
                            break;
                    }
                    else if (!free_var_list_[id])
                    {
                        if (!get_Fixed_Var(id))
                        {
                            clause_left  = CLAUSE_SAT;
                            clause_right = CLAUSE_SAT;
                            break;
                        }
                    }
                    else
                    {
                        if (clause_left == CLAUSE_UNSAT)
                            clause_left = CLAUSE_UNKNOWN;
                        if (clause_right == CLAUSE_UNSAT)
                            clause_right = CLAUSE_UNKNOWN;
                    }
                }
                else
                {//x
                    size_t id = lit - 1;
                    if (b.id_ == id)
                    {
                        ASSERT_(free_var_list_[id]);
                        clause_right = CLAUSE_SAT;//:right - x[id] = 1
                        if (clause_left != CLAUSE_UNSAT)
                            break;
                    }
                    else if (!free_var_list_[id])
                    {
                        if (get_Fixed_Var(id))
                        {
                            clause_left  = CLAUSE_SAT;
                            clause_right = CLAUSE_SAT;
                            break;
                        }
                    }
                    else
                    {
                        if (clause_left == CLAUSE_UNSAT)
                            clause_left = CLAUSE_UNKNOWN;
                        if (clause_right == CLAUSE_UNSAT)
                            clause_right = CLAUSE_UNKNOWN;
                    }
                }
            }
            switch(clause_left)
            {
            case CLAUSE_UNSAT:
                ++b.unsat_left_;
                break;
            case CLAUSE_SAT:
                ++b.sat_left_;
                break;
            }
            switch(clause_right)
            {
            case CLAUSE_UNSAT:
                ++b.unsat_right_;
                break;
            case CLAUSE_SAT:
                ++b.sat_right_;
                break;
            }
            clause += clause_length;
        }

        b.lb_left_  = b.unsat_left_;
        b.lb_right_ = b.unsat_right_;
        b.lb_max_ = std::max(b.lb_left_, b.lb_right_);

        b.sat_max_ = std::max(b.sat_left_, b.sat_right_);
    }
};
//__________________________________________________________________________________
//__________________________________________________________________________________

//EOF!
